H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 0.622 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ IFR

mainModule List

((delete :: () -> [()] -> [()]) :: () -> [()] -> [()])

module List where

import qualified Maybe
import qualified Prelude

delete :: Eq a => a -> [a] -> [a]

delete

deleteBy (==)

deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]

deleteBy	_ _ []	=	[]
deleteBy	eq x (y : ys)	=	if x `eq` y then ys else y : deleteBy eq x ys

module Maybe where

import qualified List
import qualified Prelude

If Reductions:
The following If expression

if eq x y then ys else y : deleteBy eq x ys

is transformed to

deleteBy0 ys y eq x True = ys

deleteBy0 ys y eq x False = y : deleteBy eq x ys

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

mainModule List

((delete :: () -> [()] -> [()]) :: () -> [()] -> [()])

module List where

import qualified Maybe
import qualified Prelude

delete :: Eq a => a -> [a] -> [a]

delete

deleteBy (==)

deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]

deleteBy	_ _ []	=	[]
deleteBy	eq x (y : ys)	=	deleteBy0 ys y eq x (x `eq` y)

deleteBy0	ys y eq x True	=	ys
deleteBy0	ys y eq x False	=	y : deleteBy eq x ys

module Maybe where

import qualified List
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule List

((delete :: () -> [()] -> [()]) :: () -> [()] -> [()])

module List where

import qualified Maybe
import qualified Prelude

delete :: Eq a => a -> [a] -> [a]

delete

deleteBy (==)

deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]

deleteBy	vw vx []	=	[]
deleteBy	eq x (y : ys)	=	deleteBy0 ys y eq x (x `eq` y)

deleteBy0	ys y eq x True	=	ys
deleteBy0	ys y eq x False	=	y : deleteBy eq x ys

module Maybe where

import qualified List
import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

mainModule List

(delete :: () -> [()] -> [()])

module List where

import qualified Maybe
import qualified Prelude

delete :: Eq a => a -> [a] -> [a]

delete

deleteBy (==)

deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]

deleteBy	vw vx []	=	[]
deleteBy	eq x (y : ys)	=	deleteBy0 ys y eq x (x `eq` y)

deleteBy0	ys y eq x True	=	ys
deleteBy0	ys y eq x False	=	y : deleteBy eq x ys

module Maybe where

import qualified List
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="delete",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="delete wu3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="delete wu3 wu4",fontsize=16,color="black",shape="triangle"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="deleteBy (==) wu3 wu4",fontsize=16,color="burlywood",shape="box"];14[label="wu4/wu40 : wu41",fontsize=10,color="white",style="solid",shape="box"];5 -> 14[label="",style="solid", color="burlywood", weight=9];
14 -> 6[label="",style="solid", color="burlywood", weight=3];
15[label="wu4/[]",fontsize=10,color="white",style="solid",shape="box"];5 -> 15[label="",style="solid", color="burlywood", weight=9];
15 -> 7[label="",style="solid", color="burlywood", weight=3];
6[label="deleteBy (==) wu3 (wu40 : wu41)",fontsize=16,color="black",shape="box"];6 -> 8[label="",style="solid", color="black", weight=3];
7[label="deleteBy (==) wu3 []",fontsize=16,color="black",shape="box"];7 -> 9[label="",style="solid", color="black", weight=3];
8[label="deleteBy0 wu41 wu40 (==) wu3 ((==) wu3 wu40)",fontsize=16,color="burlywood",shape="box"];16[label="wu3/()",fontsize=10,color="white",style="solid",shape="box"];8 -> 16[label="",style="solid", color="burlywood", weight=9];
16 -> 10[label="",style="solid", color="burlywood", weight=3];
9[label="[]",fontsize=16,color="green",shape="box"];10[label="deleteBy0 wu41 wu40 (==) () ((==) () wu40)",fontsize=16,color="burlywood",shape="box"];17[label="wu40/()",fontsize=10,color="white",style="solid",shape="box"];10 -> 17[label="",style="solid", color="burlywood", weight=9];
17 -> 11[label="",style="solid", color="burlywood", weight=3];
11[label="deleteBy0 wu41 () (==) () ((==) () ())",fontsize=16,color="black",shape="box"];11 -> 12[label="",style="solid", color="black", weight=3];
12[label="deleteBy0 wu41 () (==) () True",fontsize=16,color="black",shape="box"];12 -> 13[label="",style="solid", color="black", weight=3];
13[label="wu41",fontsize=16,color="green",shape="box"];}

deleteBy0	ys y eq x True	= ys
deleteBy0	ys y eq x False	= y : deleteBy eq x ys